/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓1. Introduction

␈↓ α∧␈↓␈↓ αT(McCarthy␈α∀1959)␈α∀proposed␈α∀a␈α∀program␈α∀with␈α∀"common␈α∀sense"␈α∀which␈α∀would␈α∀express␈α∪its
␈↓ α∧␈↓knowledge␈α∪about␈α∪the␈α∪world␈α∪in␈α∪general␈α∪and␈α∩about␈α∪its␈α∪present␈α∪situation␈α∪in␈α∪a␈α∪suitable␈α∩logical
␈↓ α∧␈↓language.␈α∞ It␈α∞would␈α∞then␈α∞reason␈α
in␈α∞this␈α∞language␈α∞attempting␈α∞to␈α
derive␈α∞a␈α∞sentence␈α∞of␈α∞the␈α∞form␈α
␈↓↓I
␈↓ α∧␈↓↓should␈α∂do␈α∂X␈↓␈α∂after␈α⊂which␈α∂it␈α∂would␈α∂do␈α∂␈↓↓X.␈↓␈α⊂This␈α∂approach␈α∂was␈α∂further␈α∂developed␈α⊂in␈α∂(McCarthy
␈↓ α∧␈↓1963)␈α∂and␈α∂(McCarthy␈α∞and␈α∂Hayes␈α∂1969),␈α∂but␈α∞by␈α∂1969␈α∂it␈α∂was␈α∞already␈α∂clear␈α∂that␈α∂something␈α∞more
␈↓ α∧␈↓deduction␈α
was␈αnecessary␈α
in␈α
order␈αto␈α
express␈αand␈α
use␈α
common␈αsense␈α
knowledge.␈α
 Further␈αanalysis
␈↓ α∧␈↓showed␈αthat␈αwhat␈αwas␈αmissing␈αwas␈αthe␈αability␈αto␈αjump␈αto␈αthe␈αconclusion␈αthat␈αthe␈αfacts␈αtaken␈αinto
␈↓ α∧␈↓account␈α∞are␈α
sufficient␈α∞to␈α∞solve␈α
a␈α∞problem.␈α
 How␈α∞to␈α∞express␈α
this␈α∞ability␈α
is␈α∞still␈α∞problematical,␈α
but
␈↓ α∧␈↓this paper presents one candidate.

␈↓ α∧␈↓␈↓ αT␈↓↓Circumscription␈αinduction␈↓␈α
is␈αa␈αformalized␈α
␈↓↓rule␈αof␈αconjecture␈↓␈α
that␈αcan␈αbe␈α
adjoined␈αto␈αthe␈α
␈↓↓rules
␈↓ α∧␈↓↓of␈α∩inference␈↓␈α∪of␈α∩first␈α∩order␈α∪logic.␈α∩ A␈α∪computer␈α∩program␈α∩can␈α∪use␈α∩circumscription␈α∪induction␈α∩to
␈↓ α∧␈↓conjecture␈α
that␈αthe␈α
known␈α
entities␈αof␈α
a␈α
given␈αkind␈α
are␈α
all␈αthere␈α
are.␈α
 We␈αwill␈α
show␈α
by␈αexamples
␈↓ α∧␈↓that␈αhumans␈αuse␈αsuch␈α"non-monotonic"␈αreasoning␈αand␈αthat␈αit␈αis␈αrequired␈αfor␈αintelligent␈αbehavior.
␈↓ α∧␈↓The␈αdefault␈αcase␈αreasoning␈αof␈αmany␈αcomputer␈αprograms␈αand␈αthe␈αuse␈αof␈αTHNOT␈αin␈αPLANNER
␈↓ α∧␈↓programs are examples of non-monotonic reasoning of a possibly different kind.

␈↓ α∧␈↓␈↓ αTAll␈αthe␈αsystems␈αstudied␈αin␈αmathematical␈αlogic␈αhave␈αthe␈αfollowing␈α␈↓↓monotonicity␈αproperty␈↓.␈α If␈α
a
␈↓ α∧␈↓sentence␈α∂␈↓↓p␈↓␈α∂follows␈α∂from␈α∂a␈α∞collection␈α∂␈↓↓A␈↓␈α∂of␈α∂sentences␈α∂and␈α∂␈↓↓A ⊂ B␈↓,␈α∞then␈α∂␈↓↓p␈↓␈α∂follows␈α∂from␈α∂␈↓↓B.␈↓␈α∂In␈α∞the
␈↓ α∧␈↓notation␈α
of␈α
proof␈α
theory:␈α
if␈α
␈↓↓A ␈↓πr␈↓↓ p␈↓␈α
and␈α
␈↓↓A ⊂ B␈↓,␈α
then␈α
␈↓↓B ␈↓πr␈↓↓ p␈↓.␈α
 Since␈α
a␈α
proof␈α
from␈α
the␈α
premisses␈α
␈↓↓A␈↓␈αis␈α
a
␈↓ α∧␈↓sequence␈α
of␈αsentences␈α
each␈α
of␈αwhich␈α
is␈αa␈α
either␈α
a␈αpremiss,␈α
an␈αaxiom␈α
or␈α
follows␈αfrom␈α
a␈α
subset␈αof
␈↓ α∧␈↓the␈αsentences␈α
occurring␈αearlier␈αin␈α
the␈αproof␈αby␈α
one␈αof␈αthe␈α
rules␈αof␈αinference,␈α
a␈αproof␈αfrom␈α
␈↓↓A␈↓␈αcan
␈↓ α∧␈↓also␈α∪serve␈α∪as␈α∪a␈α∪proof␈α∪from␈α∪␈↓↓B␈↓␈α∪assuming␈α∪␈↓↓A ⊂ B␈↓.␈α∪ The␈α∪semantic␈α∪notion␈α∪of␈α∪entailment␈α∪is␈α∪also
␈↓ α∧␈↓monotonic;␈αwe␈α
say␈αthat␈α
␈↓↓A␈↓␈αentails␈α
␈↓↓p␈↓␈α(written␈α
␈↓↓A ␈↓πq␈↓↓ p␈↓)␈αif␈α␈↓↓p␈↓␈α
is␈αtrue␈α
in␈αall␈α
models␈αof␈α
␈↓↓A.␈↓␈αBut␈α
if␈α␈↓↓A ␈↓πq␈↓↓ p␈↓
␈↓ α∧␈↓and␈α∂␈↓↓A ⊂ B␈↓,␈α∂then␈α∂every␈α∂model␈α∂of␈α∂␈↓↓B␈↓␈α∂is␈α∂also␈α∂a␈α∂model␈α∂of␈α∂␈↓↓A,␈↓␈α∂which␈α∂shows␈α∂that␈α∂␈↓↓B ␈↓πq␈↓↓ p␈↓.␈α⊂ Some␈α∂AI
␈↓ α∧␈↓reasoning␈α
systems␈α
are␈α
non-monotonic,␈α
because␈α
they␈αcontain␈α
rules␈α
of␈α
inference␈α
that␈α
not␈αonly␈α
require
␈↓ α∧␈↓the␈αpresence␈αpremiss␈αsentences␈αin␈αthe␈αdata␈αbase␈αmatching␈αtheir␈αpatterns␈αbut␈αrequire␈αthe␈α␈↓↓absence␈↓␈αof
␈↓ α∧␈↓sentences matching certain other patterns.

␈↓ α∧␈↓␈↓ αTThe␈α⊂result␈α∂of␈α⊂applying␈α∂circumscription␈α⊂induction␈α⊂to␈α∂a␈α⊂collection␈α∂␈↓↓A␈↓␈α⊂of␈α∂facts␈α⊂is␈α⊂a␈α∂sentence
␈↓ α∧␈↓schema␈α∞that␈α∂essentially␈α∞asserts␈α∞that␈α∂the␈α∞only␈α∞objects␈α∂satisfying␈α∞a␈α∞predicate␈α∂␈↓↓P(x)␈↓␈α∞are␈α∂those␈α∞whose
␈↓ α∧␈↓existence␈α
follows␈α
from␈α
the␈α
sentences␈α
of␈α
␈↓↓A.␈↓␈α
Since␈α
adding␈α
more␈α
sentences␈α
might␈α
require␈α
the␈α
existence
␈↓ α∧␈↓of␈αmore␈αobjects,␈αcircumscription␈αis␈αnot␈αmonotonic.␈α Conclusions␈αderived␈αfrom␈αcircumscription␈αmay
␈↓ α∧␈↓be␈αregarded␈αas␈αconsequences␈αof␈αconjecturing␈αthat␈α␈↓↓A␈↓␈αincludes␈αall␈αthe␈αrelevant␈αfacts.␈α An␈αintelligent
␈↓ α∧␈↓program␈α
might␈αmake␈α
such␈α
a␈αconjecture␈α
make␈α
a␈αplan␈α
on␈αthe␈α
basis␈α
of␈αthe␈α
conclusions␈α
reached.␈α It
␈↓ α∧␈↓might␈α⊂immediately␈α∂carry␈α⊂out␈α⊂the␈α∂plan,␈α⊂or␈α∂be␈α⊂more␈α⊂cautious␈α∂and␈α⊂look␈α∂for␈α⊂additional␈α⊂facts␈α∂that
␈↓ α∧␈↓might␈α
require␈α∞modifying␈α
it.␈α
 If␈α∞it␈α
comes␈α
to␈α∞reject␈α
the␈α
circumscription␈α∞conjecture,␈α
it␈α∞will␈α
normally
␈↓ α∧␈↓have␈α∞to␈α
circumscribe␈α∞again␈α
on␈α∞the␈α
basis␈α∞of␈α∞additional␈α
facts.␈α∞ It␈α
will␈α∞be␈α
necessary␈α∞to␈α∞␈↓↓assume␈↓␈α
that
␈↓ α∧␈↓everything␈α
relevant␈α
has␈αfinally␈α
been␈α
taken␈αinto␈α
account,␈α
except␈αin␈α
mathematical␈α
problems,␈αwhere␈α
it
␈↓ α∧␈↓can often be proved from the original statement of the problem.

␈↓ α∧␈↓␈↓ αTBefore␈α∩introducing␈α∩the␈α∩formalism,␈α∩we␈α∪present␈α∩an␈α∩example␈α∩showing␈α∩the␈α∩need␈α∪for␈α∩non-
␈↓ α∧␈↓monotonic reasoning.
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓αMissionaries and Cannibals

␈↓ α∧␈↓␈↓ αTThe␈α∞much␈α∂used␈α∞␈↓↓missionaries␈α∞and␈α∂cannibals␈↓␈α∞puzzle␈α∞contains␈α∂enough␈α∞detail␈α∞to␈α∂illustrate␈α∞the
␈↓ α∧␈↓issues.

␈↓ α∧␈↓␈↓ αT␈↓↓"Three␈α∪missionaries␈α∀and␈α∪three␈α∀cannibals␈α∪come␈α∀to␈α∪a␈α∪river.␈α∀ A␈α∪rowboat␈α∀that␈α∪seats␈α∀two␈α∪is
␈↓ α∧␈↓↓available.␈α∪ If␈α∩the␈α∪cannibals␈α∩ever␈α∪outnumber␈α∪the␈α∩missionaries␈α∪on␈α∩either␈α∪bank␈α∩of␈α∪the␈α∪river,␈α∩the
␈↓ α∧␈↓↓missionaries will be eaten.  How shall they cross the river?"␈↓.

␈↓ α∧␈↓␈↓ αTObviously␈α
the␈α∞puzzler␈α
is␈α
expected␈α∞to␈α
devise␈α
a␈α∞strategy␈α
of␈α
rowing␈α∞the␈α
boat␈α
back␈α∞and␈α
forth
␈↓ α∧␈↓that gets them all across and avoids the disaster.

␈↓ α∧␈↓␈↓ αTAmarel␈α∩(1971)␈α∩considered␈α∩several␈α∩representations␈α⊃of␈α∩the␈α∩problem␈α∩and␈α∩discussed␈α⊃criteria
␈↓ α∧␈↓whereby␈α⊂the␈α⊃following␈α⊂representation␈α⊂is␈α⊃preferred␈α⊂for␈α⊂purposes␈α⊃of␈α⊂AI,␈α⊂because␈α⊃it␈α⊂leads␈α⊃to␈α⊂the
␈↓ α∧␈↓smallest␈αstate␈αspace␈αthat␈αmust␈αbe␈αexplored␈αto␈αfind␈αthe␈αsolution.␈α A␈αstate␈αis␈αa␈αtriple␈αcomprising␈αthe
␈↓ α∧␈↓numbers␈αof␈αmissionaries,␈αcannibals␈αand␈αboats␈αon␈αthe␈αstarting␈αbank␈αof␈αthe␈αriver.␈α The␈αinitial␈αstate
␈↓ α∧␈↓is␈α≤331,␈α≤the␈α≤desired␈α≤final␈α≤state␈α≤is␈α≤000,␈α≤and␈α≤one␈α≤solution␈α≤is␈α≤given␈α≤by␈α≤the␈α≠sequence
␈↓ α∧␈↓(331,220,321,300,311,110,221,020,031,010,021,000).

␈↓ α∧␈↓␈↓ αTWe␈α⊂are␈α⊂not␈α⊂presently␈α⊂concerned␈α⊂with␈α⊂the␈α⊂heuristics␈α⊂of␈α⊂the␈α⊂problem␈α⊂but␈α⊂rather␈α⊂with␈α⊂the
␈↓ α∧␈↓correctness␈αof␈αthe␈αreasoning␈αthat␈α
goes␈αfrom␈αthe␈αEnglish␈αstatement␈α
of␈αthe␈αproblem␈αto␈αAmarel's␈α
state
␈↓ α∧␈↓space␈α
representation.␈α
 A␈α∞generally␈α
intelligent␈α
computer␈α∞program␈α
should␈α
be␈α∞able␈α
to␈α
carry␈α∞out␈α
this
␈↓ α∧␈↓reasoning.␈α⊃ Of␈α⊃course,␈α⊃there␈α⊃are␈α⊃the␈α⊃well␈α⊃known␈α⊃difficulties␈α⊃in␈α⊃making␈α⊃computers␈α⊂understand
␈↓ α∧␈↓English,␈α⊃but␈α⊃suppose␈α⊃the␈α⊃English␈α⊃sentences␈α⊃describing␈α⊃the␈α⊃problem␈α⊃have␈α⊃already␈α⊃been␈α⊃rather
␈↓ α∧␈↓directly␈α⊂translated␈α⊂into␈α⊂first␈α⊂order␈α⊂logic.␈α⊂ The␈α⊂correctness␈α⊂of␈α⊂Amarel's␈α⊂representation␈α⊂is␈α⊃not␈α⊂an
␈↓ α∧␈↓ordinary logical consequence of these sentences for two further reasons.

␈↓ α∧␈↓␈↓ αTFirst,␈α∞nothing␈α∞has␈α∞been␈α∞stated␈α∞about␈α∞the␈α∞properties␈α∞of␈α∞boats␈α∞or␈α∞even␈α∞the␈α∞fact␈α∞that␈α
rowing
␈↓ α∧␈↓across␈α∞the␈α∞river␈α
doesn't␈α∞change␈α∞the␈α∞numbers␈α
of␈α∞missionaries␈α∞or␈α∞cannibals␈α
or␈α∞the␈α∞capacity␈α∞of␈α
the
␈↓ α∧␈↓boat.␈α Indeed␈αit␈αhasn't␈αbeen␈αstated␈αthat␈αsituations␈αchange␈αas␈αa␈αresult␈αof␈αaction.␈α These␈αfacts␈αfollow
␈↓ α∧␈↓from␈α∞common␈α∞sense␈α∞knowledge,␈α∞so␈α∞let␈α∞us␈α
imagine␈α∞that␈α∞common␈α∞sense␈α∞knowledge,␈α∞or␈α∞at␈α∞least␈α
the
␈↓ α∧␈↓relevant part of it, is also expressed in first order logic.

␈↓ α∧␈↓␈↓ αTThe␈α∩second␈α⊃reason␈α∩we␈α⊃can't␈α∩␈↓↓deduce␈↓␈α∩the␈α⊃propriety␈α∩of␈α⊃Amarel's␈α∩representation␈α∩is␈α⊃deeper.
␈↓ α∧␈↓Imagine␈α
giving␈α
someone␈α
the␈α
problem,␈α
and␈α
after␈αhe␈α
puzzles␈α
for␈α
a␈α
while,␈α
he␈α
suggests␈αgoing␈α
upstream
␈↓ α∧␈↓half␈α
a␈α
mile␈α
and␈α
crossing␈α
on␈α
a␈α
bridge.␈α∞ "What␈α
bridge",␈α
you␈α
say.␈α
 "No␈α
bridge␈α
is␈α
mentioned␈α∞in␈α
the
␈↓ α∧␈↓statement␈αof␈α
the␈αproblem."␈αAnd␈α
this␈αdunce␈αreplies,␈α
"Well,␈αthey␈α
don't␈αsay␈αthere␈α
isn't␈αa␈αbridge".␈α
 You
␈↓ α∧␈↓look␈αat␈αthe␈αEnglish␈αand␈αeven␈αat␈αthe␈αtranslation␈αof␈αthe␈αEnglish␈αinto␈αfirst␈αorder␈αlogic,␈αand␈αyou␈αmust
␈↓ α∧␈↓admit␈αthat␈α
"they␈αdon't␈αsay"␈α
there␈αis␈αno␈α
bridge.␈α So␈αyou␈α
modify␈αthe␈αproblem␈α
to␈αexclude␈αbridges␈α
and
␈↓ α∧␈↓pose␈α∂it␈α∂again,␈α∂and␈α∂the␈α∂dunce␈α∂proposes␈α∂a␈α∂helicopter,␈α∂and␈α∂after␈α∂you␈α∂exclude␈α∂that,␈α∂he␈α∂proposes␈α∂a
␈↓ α∧␈↓winged horse or that the others hang onto the outside of the boat while two row.

␈↓ α∧␈↓␈↓ αTYou␈α
now␈α∞see␈α
that␈α
while␈α∞a␈α
dunce,␈α∞he␈α
is␈α
an␈α∞inventive␈α
dunce.␈α
 Despairing␈α∞of␈α
getting␈α∞him␈α
to
␈↓ α∧␈↓accept␈α⊂the␈α⊂problem␈α⊂in␈α⊂the␈α⊂proper␈α⊂puzzler's␈α⊂spirit,␈α⊂you␈α⊂tell␈α⊂him␈α⊂the␈α⊂solution.␈α⊂ To␈α⊃your␈α⊂further
␈↓ α∧␈↓annoyance,␈αhe␈αattacks␈αyour␈αsolution␈αon␈αthe␈αgrounds␈αthat␈αthe␈αboat␈αmight␈αhave␈αa␈αleak␈αor␈αlack␈αoars.
␈↓ α∧␈↓After␈αyou␈αrectify␈αthat␈αomission␈αfrom␈αthe␈αstatement␈αof␈αthe␈αproblem,␈αhe␈αsuggests␈αthat␈αa␈αsea␈αmonster
␈↓ α∧␈↓may␈αswim␈αup␈αthe␈αriver␈αand␈αmay␈αswallow␈αthe␈αboat.␈α Again␈αyou␈αare␈αfrustrated,␈αand␈αyou␈αlook␈αfor␈αa
␈↓ α∧␈↓mode of reasoning that will settle his hash once and for all.
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓␈↓ αTIn␈αspite␈α
of␈αour␈α
irritation␈αwith␈αthe␈α
dunce,␈αit␈α
would␈αbe␈αcheating␈α
to␈αput␈α
into␈αthe␈α
statement␈αof
␈↓ α∧␈↓the␈α
problem␈α
that␈α
there␈α
is␈α
no␈αother␈α
way␈α
to␈α
cross␈α
the␈α
river␈αthan␈α
using␈α
the␈α
boat␈α
and␈α
that␈αnothing␈α
can
␈↓ α∧␈↓go␈αwrong␈α
with␈αthe␈α
boat.␈α A␈αhuman␈α
doesn't␈αneed␈α
such␈αan␈αad␈α
hoc␈αnarrowing␈α
of␈αthe␈α
problem,␈αand
␈↓ α∧␈↓indeed␈αthe␈αonly␈αwatertight␈αway␈αto␈αdo␈αit␈αmight␈αamount␈αto␈αspecifying␈αthe␈αAmarel␈αrepresentation␈αin
␈↓ α∧␈↓English.␈α Rather␈α
we␈αwant␈αto␈α
avoid␈αthe␈α
excessive␈αqualification␈αand␈α
get␈αthe␈α
Amarel␈αrepresentation
␈↓ α∧␈↓by common sense reasoning as humans ordinarily do.

␈↓ α∧␈↓␈↓ αTCircumscription␈αis␈αone␈αcandidate␈αfor␈αaccomplishing␈αthis.␈α It␈αwill␈αallow␈αus␈αto␈αconjecture␈αthat
␈↓ α∧␈↓no␈αrelevant␈α
entities␈αexist␈αexcept␈α
those␈αwhose␈αexistence␈α
follows␈αfrom␈αthe␈α
statement␈αof␈α
the␈αproblem
␈↓ α∧␈↓and␈α∩common␈α∪sense␈α∩knowledge.␈α∩ When␈α∪we␈α∩␈↓↓circumscribe␈↓␈α∪the␈α∩first␈α∩order␈α∪logic␈α∩statement␈α∪of␈α∩the
␈↓ α∧␈↓problem␈α
together␈α
with␈α
the␈α
common␈α
sense␈α
facts␈α
about␈α
boats␈α
etc.,␈α
we␈α
will␈α
be␈α
able␈α
to␈α
conclude␈α
that
␈↓ α∧␈↓there␈αis␈αno␈αbridge␈αor␈αhelicopter.␈α "Aha",␈αyou␈αsay,␈α"but␈αthere␈αwon't␈αbe␈αany␈αoars␈αeither".␈α No,␈αwe␈αget
␈↓ α∧␈↓out␈αof␈αthat␈αas␈αfollows:␈αIt␈αis␈αa␈αpart␈αof␈αcommon␈αknowledge␈αthat␈αa␈αboat␈αcan␈αbe␈αused␈αto␈αcross␈αa␈αriver
␈↓ α∧␈↓␈↓↓unless␈αthere␈αis␈αsomething␈α
wrong␈αwith␈αit␈αor␈α
something␈αelse␈αprevents␈αusing␈α
it␈↓,␈αand␈αif␈αour␈α
facts␈αdon't
␈↓ α∧␈↓require␈αthat␈αthere␈αbe␈αsomething␈αthat␈αprevents␈αcrossing␈αthe␈αriver,␈αcircumscription␈αwill␈αgenerate␈αthe
␈↓ α∧␈↓conjecture␈αthat␈α
there␈αisn't.␈α
 The␈αprice␈α
is␈αintroducing␈αas␈α
entities␈αin␈α
our␈αlanguage␈α
the␈α"somethings"
␈↓ α∧␈↓that may prevent the use of the boat.

␈↓ α∧␈↓␈↓ αTIf␈α
the␈αstatement␈α
of␈α
the␈αproblem␈α
were␈α
extended␈αto␈α
mention␈α
a␈αbridge,␈α
then␈αthe␈α
circumscription
␈↓ α∧␈↓of␈α∞the␈α∞problem␈α∞statement␈α∞would␈α∞no␈α∞longer␈α∂permit␈α∞showing␈α∞the␈α∞non-existence␈α∞of␈α∞a␈α∞bridge,␈α∂i.e.␈α∞a
␈↓ α∧␈↓conclusion␈α
that␈α
can␈α
be␈α∞drawn␈α
from␈α
a␈α
smaller␈α∞collection␈α
of␈α
facts␈α
can␈α∞no␈α
longer␈α
be␈α
drawn␈α∞from␈α
a
␈↓ α∧␈↓larger.␈α∞ This␈α∞non-monotonic␈α∞character␈α∞of␈α∞circumscription␈α∞is␈α
just␈α∞what␈α∞we␈α∞want␈α∞for␈α∞this␈α∞kind␈α
of
␈↓ α∧␈↓problem.␈α∞ The␈α∞statement,␈α∞␈↓↓"There␈α∞is␈α∞a␈α∞bridge␈α∞a␈α
mile␈α∞upstream,␈α∞and␈α∞the␈α∞boat␈α∞has␈α∞a␈α∞leak."␈↓␈α
doesn't
␈↓ α∧␈↓contradict the text of the problem, but its addition invalidates the Amarel representation.

␈↓ α∧␈↓␈↓ αTIn␈αthe␈αusual␈αsort␈αof␈αpuzzle,␈αthere␈αis␈αa␈αconvention␈αthat␈αthere␈αis␈αno␈αadditional␈αobjects␈αbeyond
␈↓ α∧␈↓those␈αmentioned␈αin␈αthe␈αpuzzle␈αor␈αwhose␈αexistence␈αis␈αdeducible␈αfrom␈αthe␈αpuzzle␈αand␈αcommon␈αsense
␈↓ α∧␈↓knowledge.␈α The␈αconvention␈αcan␈αbe␈αexplicated␈α
as␈αapplying␈αcircumscription␈αto␈αthe␈αpuzzle␈α
statement
␈↓ α∧␈↓and␈α∞a␈α∞certain␈α∞part␈α∞of␈α∞common␈α∞sense␈α∞knowledge.␈α∞ However,␈α∞if␈α∞one␈α∞really␈α∞were␈α∞sitting␈α∞by␈α∞a␈α
river
␈↓ α∧␈↓bank␈α→and␈α_these␈α→six␈α_people␈α→came␈α→by␈α_and␈α→posed␈α_their␈α→problem,␈α_one␈α→wouldn't␈α→take␈α_the
␈↓ α∧␈↓circumscription␈α
for␈αgranted,␈α
but␈αone␈α
would␈αconsider␈α
the␈αresult␈α
of␈αcircumscripion␈α
as␈α
a␈αhypothesis.
␈↓ α∧␈↓Thus circumscription must be used as a mode of conjecture.

␈↓ α∧␈↓␈↓ αTAt␈α⊂first␈α⊂I␈α⊂considered␈α⊂this␈α⊂solution␈α⊂ad␈α⊂hoc,␈α⊂but␈α⊂I␈α⊂am␈α⊂now␈α⊂convinced␈α⊂that␈α⊂it␈α⊂is␈α⊃a␈α⊂correct
␈↓ α∧␈↓explication␈αof␈αthe␈αuse␈αof␈α␈↓↓normality␈↓;␈αi.e.␈αunless␈αsomething␈αabnormal␈αexists,␈αan␈αobject␈αcan␈αbe␈αused␈α
to
␈↓ α∧␈↓carry out its normal function.

␈↓ α∧␈↓␈↓ αTSome␈α∂have␈α∂suggested␈α∂that␈α∂the␈α∂difficulties␈α∂might␈α∂be␈α∂avoided␈α∂by␈α∂introducing␈α∂probabilities.
␈↓ α∧␈↓They␈α∞suggest␈α∞that␈α∞the␈α
existence␈α∞of␈α∞a␈α∞bridge␈α∞is␈α
improbable.␈α∞ Well,␈α∞the␈α∞whole␈α∞situation␈α
involving
␈↓ α∧␈↓cannibals␈α∂with␈α⊂the␈α∂postulated␈α⊂properties␈α∂is␈α⊂so␈α∂improbable␈α⊂that␈α∂it␈α⊂is␈α∂hard␈α⊂to␈α∂take␈α⊂seriously␈α∂the
␈↓ α∧␈↓conditional␈α⊃probability␈α⊃of␈α∩a␈α⊃bridge␈α⊃given␈α⊃the␈α∩hypotheses.␈α⊃ Moreover,␈α⊃we␈α⊃mentally␈α∩propose␈α⊃to
␈↓ α∧␈↓ourselves␈α~the␈α~normal␈α≠non-bridge␈α~non-sea-monster␈α~interpretation␈α~␈↓↓before␈↓␈α≠considering␈α~these
␈↓ α∧␈↓extraneous␈α
possibilities,␈α
let␈α
alone␈α
their␈α
probabilities,␈α
i.e.␈α
we␈α
usually␈α
don't␈α
even␈α
introduce␈α
the␈α
sample
␈↓ α∧␈↓space␈αin␈αwhich␈αthese␈αpossibilities␈αare␈αassigned␈αwhatever␈αprobabilities␈αone␈αmight␈αconsider␈αthem␈αto
␈↓ α∧␈↓have.␈α Therefore,␈αregardless␈αof␈αour␈αknowledge␈αof␈αprobabilities,␈αwe␈αneed␈αa␈αway␈αof␈αformulating␈αthe
␈↓ α∧␈↓normal␈α∩situation␈α∩from␈α∩the␈α⊃statement␈α∩of␈α∩the␈α∩facts,␈α⊃and␈α∩non-monotonic␈α∩reasoning␈α∩seems␈α∩to␈α⊃be
␈↓ α∧␈↓required.

␈↓ α∧␈↓␈↓ αTUsing␈α
circumscription␈α
requires␈α
that␈α
common␈α
sense␈α
knowledge␈α
be␈α
expressed␈α
in␈α
a␈α∞form␈α
that
␈↓ α∧␈↓␈↓ u4


␈↓ α∧␈↓says␈α
a␈αboat␈α
can␈αbe␈α
used␈αto␈α
cross␈αrivers␈α
unless␈αthere␈α
is␈αsomething␈α
wrong␈αwith␈α
it.␈α In␈α
particular,␈αit
␈↓ α∧␈↓looks␈α⊂like␈α⊂we␈α∂must␈α⊂introduce␈α⊂into␈α⊂our␈α∂␈↓↓ontology␈↓␈α⊂(the␈α⊂things␈α⊂that␈α∂exist)␈α⊂a␈α⊂category␈α⊂that␈α∂includes
␈↓ α∧␈↓␈↓↓something␈α⊃wrong␈α⊃with␈α⊃a␈α⊃boat␈↓␈α⊃or␈α⊃a␈α⊃category␈α⊃that␈α⊃includes␈α⊃␈↓↓something␈α⊃that␈α⊃may␈α⊃prevent␈α∩its␈α⊃use␈↓.
␈↓ α∧␈↓Incidentally,␈α∂once␈α∂we␈α∂have␈α∂decided␈α∂to␈α∂admit␈α∞␈↓↓something␈α∂wrong␈α∂with␈α∂the␈α∂boat␈↓,␈α∂we␈α∂are␈α∂inclined␈α∞to
␈↓ α∧␈↓admit␈α
a␈α
␈↓↓lack␈α
of␈αoars␈↓␈α
as␈α
such␈α
a␈αsomething␈α
and␈α
to␈α
ask␈αquestions␈α
like,␈α
␈↓↓"Is␈α
a␈αlack␈α
of␈α
oars␈α
all␈α
that␈αis
␈↓ α∧␈↓↓wrong with the boat?␈↓".

␈↓ α∧␈↓␈↓ αTI␈α∩imagine␈α∩that␈α∪many␈α∩philosophers␈α∩and␈α∩scientists␈α∪would␈α∩be␈α∩reluctant␈α∩to␈α∪introduce␈α∩such
␈↓ α∧␈↓␈↓↓things,␈↓␈α
but␈α
the␈αfact␈α
that␈α
ordinary␈α
language␈αallows␈α
␈↓↓"something␈α
wrong␈αwith␈α
the␈α
boat"␈↓␈α
suggests␈αthat
␈↓ α∧␈↓we␈α
shouldn't␈α
be␈α
hasty␈α
in␈α
excluding␈α
it.␈α
 Making␈α
a␈α
suitable␈α
formalism␈α
may␈α
be␈α
technically␈αdifficult
␈↓ α∧␈↓and philosophically problematical, but we must try.

␈↓ α∧␈↓␈↓ αTWe␈α⊃challenge␈α⊂anyone␈α⊃who␈α⊃thinks␈α⊂he␈α⊃can␈α⊃avoid␈α⊂such␈α⊃entities␈α⊃to␈α⊂express␈α⊃in␈α⊃his␈α⊂favorite
␈↓ α∧␈↓formalism,␈α
␈↓↓"Besides␈αleakiness,␈α
there␈α
is␈αsomething␈α
else␈α
wrong␈αwith␈α
the␈α
boat"␈↓.␈α A␈α
good␈αsolution␈α
would
␈↓ α∧␈↓avoid counterfactuals as this one does.

␈↓ α∧␈↓␈↓ αTWe␈α∩hope␈α⊃circumscription␈α∩will␈α⊃help␈α∩understand␈α⊃natural␈α∩language,␈α⊃because␈α∩if␈α⊃the␈α∩use␈α⊃of
␈↓ α∧␈↓natural␈αlanguage␈αinvolves␈αsomething␈αlike␈αcircumscription,␈αit␈αis␈αunderstandable␈αthat␈αthe␈αexpression
␈↓ α∧␈↓of general common sense facts into natural language will seem implausible.

␈↓ α∧␈↓α␈↓ β⊗CIRCUMSCRIPTION - A FORM OF NON-MONOTONIC REASONING

␈↓ α∧␈↓2. Introduction - the need for non-monotonic reasoning

␈↓ α∧␈↓␈↓ αTHumans␈α⊂and␈α⊂intelligent␈α⊂computer␈α⊂programs␈α⊂must␈α⊂often␈α⊂jump␈α⊂to␈α⊂the␈α⊂conclusion␈α⊂that␈α⊂the
␈↓ α∧␈↓objects␈α∂they␈α∂know␈α∂about␈α⊂in␈α∂a␈α∂certain␈α∂class␈α⊂are␈α∂the␈α∂only␈α∂objects␈α⊂that␈α∂have␈α∂to␈α∂be␈α⊂considered␈α∂in
␈↓ α∧␈↓solving␈α∃a␈α∃certain␈α∃problem.␈α∃ ␈↓↓Circumscription␈α∃induction␈↓␈α∃is␈α∃one␈α∃formalization␈α∃of␈α∃this␈α∃kind␈α∀of
␈↓ α∧␈↓approximate reasoning.

␈↓ α∧␈↓␈↓ αTWhile␈αit␈αis␈αoften␈αconvenient␈αto␈αrepresent␈αinformation␈αby␈αsentences␈αin␈αa␈αmathematical␈αlogical
␈↓ α∧␈↓system,␈α∂such␈α∂as␈α∂a␈α∂first␈α∂order␈α∂language␈α∂appropriate␈α∂to␈α∂a␈α∂given␈α∂problem␈α∂domain␈α∂and␈α∂to␈α∂use␈α∞the
␈↓ α∧␈↓logical␈α⊂rules␈α∂of␈α⊂inference␈α∂to␈α⊂reason␈α∂towards␈α⊂a␈α∂solution␈α⊂of␈α∂a␈α⊂problem,␈α∂the␈α⊂rules␈α∂of␈α⊂inference␈α∂of
␈↓ α∧␈↓mathematical logic have always been monotonic.

␈↓ α∧␈↓␈↓ αTHumans␈α⊃and␈α⊂many␈α⊃computer␈α⊃programs␈α⊂designed␈α⊃to␈α⊂behave␈α⊃intelligently␈α⊃represent␈α⊂much
␈↓ α∧␈↓information␈α
as␈αsentences␈α
in␈α
some␈αlanguage␈α
and␈αsolve␈α
problems␈α
by␈αinferring␈α
further␈αsentences␈α
from
␈↓ α∧␈↓previous␈α
sentences.␈α
 An␈α
action␈α∞is␈α
performed␈α
when␈α
it␈α
is␈α∞concluded␈α
that␈α
the␈α
action␈α∞is␈α
appropriate.
␈↓ α∧␈↓The␈α∞most␈α
straightforward␈α∞approach␈α
is␈α∞to␈α
represent␈α∞the␈α
information␈α∞as␈α
sentences␈α∞in␈α
a␈α∞␈↓↓first␈α
order
␈↓ α∧␈↓↓language␈↓␈αappropriate␈αto␈αthe␈αproblem␈αdomain␈αand␈αto␈αreason␈αby␈αapplying␈αthe␈αrules␈αof␈αinference␈αof
␈↓ α∧␈↓first␈α
order␈α
logic.␈α
 Other␈α
systems␈α
of␈α
mathematical␈αlogic␈α
may␈α
be␈α
used,␈α
but␈α
this␈α
doesn't␈α
make␈αmuch
␈↓ α∧␈↓difference, because any other theory can be modelled in a first order theory.

␈↓ α∧␈↓␈↓ αTThis␈α∂paper␈α∞formalizes␈α∂a␈α∂form␈α∞of␈α∂non-monotonic␈α∂reasoning␈α∞called␈α∂␈↓↓circumscription␈↓␈α∂that␈α∞we
␈↓ α∧␈↓believe␈αis␈αused␈αby␈αhumans␈αand␈αrequired␈α
for␈αcomputer␈αprograms␈αthat␈αsolve␈αproblems␈αby␈α
intelligent
␈↓ α∧␈↓reasoning from premisses.

␈↓ α∧␈↓␈↓ αTHuman␈α⊂intelligence␈α∂has␈α⊂and␈α∂artificial␈α⊂intelligence␈α∂requires␈α⊂a␈α∂form␈α⊂of␈α⊂reasoning␈α∂different
␈↓ α∧␈↓from␈αthat␈αincluded␈αin␈αmathematical␈αlogic.␈α All␈αthe␈αsystems␈αstudied␈αin␈αmathematical␈αlogic␈αhave␈αthe
␈↓ α∧␈↓following␈α⊂␈↓↓monotonicity␈α⊃property␈↓.␈α⊂ If␈α⊂a␈α⊃sentence␈α⊂␈↓↓p␈↓␈α⊂follows␈α⊃from␈α⊂a␈α⊂collection␈α⊃␈↓↓A␈↓␈α⊂of␈α⊃sentences␈α⊂and
␈↓ α∧␈↓␈↓ u5


␈↓ α∧␈↓␈↓↓A ⊂ B␈↓,␈α
the␈α∞␈↓↓p␈↓␈α
follows␈α∞from␈α
␈↓↓B.␈↓␈α∞In␈α
the␈α∞notation␈α
of␈α∞proof␈α
theory:␈α∞if␈α
␈↓↓A ␈↓πr␈↓↓ p␈↓␈α∞and␈α
␈↓↓A ⊂ B␈↓,␈α∞then␈α
␈↓↓B ␈↓πr␈↓↓ p␈↓.
␈↓ α∧␈↓Monotonicity␈α
is␈α
a␈α
consequence␈α
of␈α
the␈α
notion␈α
of␈α
a␈α
proof␈α
as␈α
a␈α
sequence␈α
of␈α
sentences␈α
each␈α
of␈αwhich␈α
is
␈↓ α∧␈↓a␈αeither␈αa␈αpremiss␈αor␈αfollows␈αfrom␈αa␈αsubset␈αof␈αthe␈αsentences␈αoccurring␈αearlier␈αin␈αthe␈αproof␈αby␈αone
␈↓ α∧␈↓of␈αthe␈αrules␈αof␈αinference.␈α Rules␈αof␈αinference␈αin␈αlogic␈αare␈αthemselves␈α␈↓↓monotonic␈↓␈αin␈αthat␈αapplying␈αa
␈↓ α∧␈↓rule␈αrequires␈αthat␈αits␈α
premiss␈αsentences␈αbe␈αpresent␈αearlier␈α
in␈αthe␈αproof␈αbut␈αmakes␈α
no␈αrequirement
␈↓ α∧␈↓that certain sentences not be present.

␈↓ α∧␈↓␈↓ αTWe␈α⊂envisage␈α⊂using␈α⊂minimal␈α⊂inference␈α⊂in␈α⊂AI␈α∂as␈α⊂follows:␈α⊂Suppose␈α⊂a␈α⊂system␈α⊂has␈α⊂a␈α∂certain
␈↓ α∧␈↓collection␈α∞of␈α∞facts.␈α∞ It␈α∞may␈α∞or␈α∂may␈α∞not␈α∞have␈α∞all␈α∞the␈α∞relevant␈α∂facts,␈α∞but␈α∞it␈α∞is␈α∞reasonable␈α∞for␈α∂it␈α∞to
␈↓ α∧␈↓conjecture␈α∞that␈α∞does␈α∞and␈α
examine␈α∞the␈α∞consequences␈α∞of␈α
the␈α∞conjecture.␈α∞ The␈α∞minimal␈α
completion
␈↓ α∧␈↓axiom␈α
for␈αa␈α
set␈α
of␈αstatements␈α
is␈α
an␈αexpression␈α
of␈α
the␈αhypothesis␈α
that␈α
the␈αonly␈α
objects␈α
that␈αexist␈α
are
␈↓ α∧␈↓those␈α⊃which␈α⊂must␈α⊃exist␈α⊂on␈α⊃the␈α⊂basis␈α⊃of␈α⊃these␈α⊂statements.␈α⊃ In␈α⊂order␈α⊃to␈α⊂make␈α⊃this␈α⊃workable␈α⊂in
␈↓ α∧␈↓practice,␈αit␈αwill␈αbe␈αnecessary␈αto␈αapply␈αminimal␈αcompletion␈αto␈αsubsets␈αof␈αthe␈αfacts;␈αdifferent␈αsubsets
␈↓ α∧␈↓will␈αgive␈α
rise␈αto␈α
different␈αconjectures.␈α Moreover,␈α
we␈αwill␈α
need␈αto␈αapply␈α
the␈αrelativization␈α
to␈αonly
␈↓ α∧␈↓some␈α∞of␈α∞the␈α∂sorts␈α∞of␈α∞individuals,␈α∞so␈α∂that␈α∞we␈α∞can␈α∞remain␈α∂noncommittal␈α∞about␈α∞whether␈α∂there␈α∞are
␈↓ α∧␈↓more of certain sorts than our axioms prove to exist.

␈↓ α∧␈↓␈↓ αTAn␈α∩example␈α∩that␈α∩has␈α∩been␈α∩much␈α∩studied␈α⊃in␈α∩AI␈α∩and␈α∩which␈α∩contains␈α∩enough␈α∩detail␈α⊃to
␈↓ α∧␈↓illustrate various issues is the ␈↓↓missionaries and cannibals␈↓ problem, stated as follows:

␈↓ α∧␈↓␈↓ αT␈↓↓"Three␈α∪missionaries␈α∀and␈α∪three␈α∀cannibals␈α∪come␈α∀to␈α∪a␈α∪river.␈α∀ A␈α∪rowboat␈α∀that␈α∪seats␈α∀two␈α∪is
␈↓ α∧␈↓↓available.␈α
 However,␈αif␈α
the␈αcannibals␈α
ever␈αoutnumber␈α
the␈αmissionaries␈α
on␈αeither␈α
bank␈αof␈α
the␈αriver,
␈↓ α∧␈↓↓the outnumbered missionaries will be eaten.  How shall they cross the river?"␈↓.

␈↓ α∧␈↓␈↓ αTAmarel␈α⊃(1971)␈α⊃considered␈α⊃various␈α⊃representations␈α⊃of␈α⊃the␈α⊃problem␈α⊃and␈α∩discussed␈α⊃criteria
␈↓ α∧␈↓whereby␈α⊂the␈α⊃following␈α⊂representation␈α⊂is␈α⊃preferred␈α⊂for␈α⊂purposes␈α⊃of␈α⊂AI,␈α⊂because␈α⊃it␈α⊂leads␈α⊃to␈α⊂the
␈↓ α∧␈↓smallest␈αstate␈αspace␈αthat␈αmust␈αbe␈αexplored␈αto␈αfind␈αthe␈αsolution.␈α We␈αrepresent␈αa␈αstate␈αby␈αthe␈α
triplet
␈↓ α∧␈↓consisting␈α∞of␈α∞the␈α
numbers␈α∞of␈α∞missionaries,␈α
cannibals␈α∞and␈α∞boats␈α
on␈α∞the␈α∞initial␈α
bank␈α∞of␈α∞the␈α
river.
␈↓ α∧␈↓The␈αinitial␈αconfiguration␈α
is␈α331,␈αthe␈αdesired␈α
final␈αconfiguration␈αis␈α000,␈α
and␈αone␈αsolution␈α
is␈αgiven
␈↓ α∧␈↓by the sequence (331,220,321,300,311,110,221,020,031,010,021,000) of states.

␈↓ α∧␈↓␈↓ αTWe␈α⊂are␈α⊂not␈α⊂presently␈α⊂concerned␈α⊂with␈α⊂the␈α⊂heuristics␈α⊂of␈α⊂the␈α⊂problem␈α⊂but␈α⊂rather␈α⊂with␈α⊂the
␈↓ α∧␈↓correctness␈αof␈αthe␈αreasoning␈αthat␈α
goes␈αfrom␈αthe␈αEnglish␈αstatement␈α
of␈αthe␈αproblem␈αto␈αAmarel's␈α
state
␈↓ α∧␈↓space␈α
representation.␈α
 A␈α∞generally␈α
intelligent␈α
computer␈α∞program␈α
should␈α
be␈α∞able␈α
to␈α
carry␈α∞out␈α
this
␈↓ α∧␈↓reasoning.␈α⊃ Of␈α∩course␈α⊃there␈α∩are␈α⊃the␈α⊃well␈α∩known␈α⊃difficulties␈α∩in␈α⊃making␈α∩computers␈α⊃understand
␈↓ α∧␈↓English,␈α⊃but␈α⊃suppose␈α⊃the␈α⊃English␈α⊃sentences␈α⊃describing␈α⊃the␈α⊃problem␈α⊃have␈α⊃already␈α⊃been␈α⊃rather
␈↓ α∧␈↓directly␈α⊂translated␈α⊂into␈α⊂first␈α⊂order␈α⊂logic.␈α⊂ The␈α⊂correctness␈α⊂of␈α⊂Amarel's␈α⊂representation␈α⊂is␈α⊃not␈α⊂an
␈↓ α∧␈↓ordinary logical consequence of these sentences for two further reasons.

␈↓ α∧␈↓␈↓ αTFirst,␈α∞nothing␈α∞has␈α∞been␈α∞stated␈α∞about␈α∞the␈α∞properties␈α∞of␈α∞boats␈α∞or␈α∞even␈α∞the␈α∞fact␈α∞that␈α
rowing
␈↓ α∧␈↓across␈α∞the␈α∞river␈α
doesn't␈α∞change␈α∞the␈α∞numbers␈α
of␈α∞missionaries␈α∞or␈α∞cannibals␈α
or␈α∞the␈α∞capacity␈α∞of␈α
the
␈↓ α∧␈↓boat.␈α These␈αare␈αa␈αconsequence␈αof␈αcommon␈αsense␈αknowledge,␈αso␈αlet␈αus␈αimagine␈αthat␈αcommon␈αsense
␈↓ α∧␈↓knowledge, or at least the relevant part of it, is also expressed in first order logic.

␈↓ α∧␈↓␈↓ αTThe␈α∩second␈α⊃reason␈α∩we␈α⊃can't␈α∩␈↓↓deduce␈↓␈α∩the␈α⊃propriety␈α∩of␈α⊃Amarel's␈α∩representation␈α∩is␈α⊃deeper.
␈↓ α∧␈↓Imagine␈α
giving␈α
someone␈α
the␈α
problem,␈α
and␈α
after␈αhe␈α
puzzles␈α
for␈α
a␈α
while,␈α
he␈α
suggests␈αgoing␈α
upstream
␈↓ α∧␈↓half␈α
a␈α
mile␈α
and␈α
crossing␈α
on␈α
a␈α
bridge.␈α∞ "What␈α
bridge",␈α
you␈α
say.␈α
 "No␈α
bridge␈α
is␈α
mentioned␈α∞in␈α
the
␈↓ α∧␈↓statement␈αof␈αthe␈α
problem."␈αAnd␈αthis␈α
dunce␈αreplies,␈α"Well,␈α
it␈αisn't␈αstated␈α
that␈αthere␈αisn't␈α
a␈αbridge".
␈↓ α∧␈↓You␈αlook␈αat␈αthe␈αEnglish␈αand␈αeven␈αat␈αthe␈αtranslation␈αof␈αthe␈αEnglish␈αinto␈αfirst␈αorder␈αlogic,␈αand␈αyou
␈↓ α∧␈↓␈↓ u6


␈↓ α∧␈↓must␈α∂admit␈α∞that␈α∂it␈α∞isn't␈α∂stated␈α∂that␈α∞there␈α∂is␈α∞no␈α∂bridge.␈α∂ So␈α∞you␈α∂modify␈α∞the␈α∂problem␈α∂to␈α∞exclude
␈↓ α∧␈↓bridges␈α∞and␈α∞pose␈α∂it␈α∞again,␈α∞and␈α∂the␈α∞dunce␈α∞proposes␈α∂a␈α∞helicopter,␈α∞and␈α∂after␈α∞you␈α∞exclude␈α∂that␈α∞he
␈↓ α∧␈↓proposes␈αa␈α
winged␈αhorse␈αor␈α
that␈αthe␈α
others␈αhang␈αonto␈α
the␈αoutside␈α
of␈αthe␈αboat␈α
while␈αtwo␈αrow.␈α
 You
␈↓ α∧␈↓now␈α
see␈α
that␈α
while␈α
a␈α
dunce,␈α
he␈α
is␈α
an␈αinventive␈α
dunce,␈α
and␈α
you␈α
despair␈α
of␈α
getting␈α
him␈α
to␈αaccept␈α
the
␈↓ α∧␈↓problem␈αin␈α
the␈αproper␈α
puzzler's␈αspirit␈α
and␈αtell␈α
him␈αthe␈α
solution.␈α You␈α
are␈αfurther␈α
annoyed␈αwhen
␈↓ α∧␈↓he␈αattacks␈αyour␈αsolution␈αon␈αthe␈αgrounds␈αthat␈αthe␈αboat␈αmight␈αhave␈αa␈αleak␈αor␈αnot␈αhave␈αoars.␈α After
␈↓ α∧␈↓you␈αrectify␈αthat␈αomission,␈αhe␈αsuggests␈αthat␈αa␈αsea␈αmonster␈αmay␈αswim␈αup␈αthe␈αriver␈αand␈αmay␈αswallow
␈↓ α∧␈↓the␈αboat.␈α
 Again␈αyou␈α
are␈αfrustrated,␈α
and␈αyou␈α
look␈αfor␈α
a␈αmode␈α
of␈αreasoning␈α
that␈αwill␈α
settle␈αhis␈α
hash
␈↓ α∧␈↓once and for all.

␈↓ α∧␈↓␈↓ αTMinimal␈αmodels␈α
and␈αminimal␈αinference␈α
may␈αgive␈αthe␈α
solution.␈α In␈αa␈α
minimal␈αmodel␈α
of␈αthe
␈↓ α∧␈↓first␈α∞order␈α
logic␈α∞statement␈α
of␈α∞the␈α
problem,␈α∞there␈α∞is␈α
no␈α∞bridge␈α
or␈α∞helicopter.␈α
 "Ah",␈α∞you␈α∞say,␈α
"but
␈↓ α∧␈↓there␈αaren't␈αany␈αoars␈αeither".␈α No,␈αwe␈αget␈αout␈αof␈αthat␈αas␈αfollows:␈αIt␈αis␈αa␈αpart␈αof␈αcommon␈αknowledge
␈↓ α∧␈↓that␈αa␈αboat␈αcan␈αbe␈αused␈αto␈αcross␈αa␈αriver␈α␈↓↓unless␈αthere␈αis␈αsomething␈αwrong␈αwith␈αit␈αor␈α
something␈αelse
␈↓ α∧␈↓↓prevents␈αusing␈αit␈↓,␈αand␈αin␈αthe␈αminimal␈αmodel␈αof␈αthe␈αfacts␈αthere␈αdoesn't␈αexist␈αsomething␈αwrong␈α
with
␈↓ α∧␈↓the boat, and there isn't anything else to prevent its use.

␈↓ α∧␈↓␈↓ αTThe␈α∪non-monotonic␈α∩character␈α∪of␈α∩minimal␈α∪reasoning␈α∪is␈α∩just␈α∪what␈α∩we␈α∪want␈α∪here.␈α∩ The
␈↓ α∧␈↓statement,␈α␈↓↓"There␈αis␈αa␈αbridge␈α
a␈αmile␈αupstream."␈↓␈αdoesn't␈αcontradict␈α
the␈αtext␈αof␈αthe␈αproblem,␈α
but␈αits
␈↓ α∧␈↓addition invalidates the Amarel representation.

␈↓ α∧␈↓␈↓ αTIn␈α∞the␈α∞usual␈α∞sort␈α∞of␈α∞puzzle,␈α∞there␈α∞can␈α∞be␈α∞no␈α∞additional␈α∞source␈α∞of␈α∞information␈α∞beyond␈α∞the
␈↓ α∧␈↓puzzle␈αand␈αcommon␈αsense␈α
knowledge.␈α Therefore,␈αthe␈αconvention␈α
can␈αbe␈αexplicated␈αas␈α
taking␈αthe
␈↓ α∧␈↓minimal␈α∞completion␈α∞of␈α∞the␈α
puzzle␈α∞statement␈α∞and␈α∞a␈α∞certain␈α
part␈α∞of␈α∞common␈α∞sense␈α∞knowledge.␈α
 If
␈↓ α∧␈↓one␈α
really␈α
were␈αsitting␈α
by␈α
a␈α
river␈αbank␈α
and␈α
these␈αsix␈α
people␈α
came␈α
by␈αand␈α
posed␈α
their␈αproblem,␈α
one
␈↓ α∧␈↓wouldn't␈α∂immediately␈α∞take␈α∂the␈α∞minimal␈α∂completion␈α∂for␈α∞granted,␈α∂but␈α∞one␈α∂would␈α∞consider␈α∂it␈α∂as␈α∞a
␈↓ α∧␈↓hypothesis.

␈↓ α∧␈↓␈↓ αTAt␈αfirst␈αI␈αconsidered␈αthis␈αsolution␈αtoo␈αad␈αhoc␈αto␈αbe␈αacceptable,␈αbut␈αI␈αam␈αnow␈αconvinced␈αthat
␈↓ α∧␈↓it␈αis␈αa␈αcorrect␈αexplication␈αof␈αthe␈α␈↓↓normal␈↓␈αsituation,␈αe.g.␈αunless␈αsomething␈αabnormal␈αexists,␈αan␈αobject
␈↓ α∧␈↓can be used to carry out its normal function.

␈↓ α∧␈↓␈↓ αTSome␈α∂have␈α∂suggested␈α∂that␈α∂the␈α∂difficulties␈α∂might␈α∂be␈α∂avoided␈α∂by␈α∂introducing␈α∂probabilities.
␈↓ α∧␈↓They␈α∞suggest␈α∞that␈α∞the␈α∂existence␈α∞of␈α∞a␈α∞bridge␈α∞is␈α∂improbable.␈α∞ Well␈α∞the␈α∞whole␈α∂situation␈α∞involving
␈↓ α∧␈↓cannibals␈α∂with␈α⊂the␈α∂postulated␈α⊂properties␈α∂is␈α⊂so␈α∂improbable␈α⊂that␈α∂it␈α⊂is␈α∂hard␈α⊂to␈α∂take␈α⊂seriously␈α∂the
␈↓ α∧␈↓conditional␈α⊃probability␈α⊃of␈α∩a␈α⊃bridge␈α⊃given␈α⊃the␈α∩hypotheses.␈α⊃ Moreover,␈α⊃we␈α⊃mentally␈α∩propose␈α⊃to
␈↓ α∧␈↓ourselves␈α→the␈α→normal␈α→non-bridge␈α→non-sea␈α→monster␈α→interpretation␈α→␈↓↓before␈↓␈α→considering␈α_these
␈↓ α∧␈↓extraneous␈α
possibilities,␈α
let␈α
alone␈α
their␈α
probabilities,␈α
i.e.␈α
we␈α
usually␈α
don't␈α
even␈α
introduce␈α
the␈α
sample
␈↓ α∧␈↓space␈αin␈αwhich␈αthese␈αpossibilities␈αare␈αassigned␈αwhatever␈αprobabilities␈αone␈αmight␈αconsider␈αthem␈αto
␈↓ α∧␈↓have.␈α Therefore,␈αregardless␈αof␈αour␈αknowledge␈αof␈αprobabilities,␈αwe␈αneed␈αa␈αway␈αof␈αformulating␈αthe
␈↓ α∧␈↓normal␈α
situation␈α
from␈α
the␈α
statement␈α
of␈α
the␈α
facts,␈α
and␈α
the␈α
minimal␈α
completion␈α
axioms␈α
seems␈α
to␈α
be␈α
a
␈↓ α∧␈↓method.

␈↓ α∧␈↓␈↓ αTOf␈αcourse,␈αwe␈αhaven't␈αgiven␈αan␈αexpression␈αof␈αcommon␈αsense␈αknowledge␈αin␈αa␈αform␈αthat␈αsays
␈↓ α∧␈↓a␈α∂boat␈α∂can␈α⊂be␈α∂used␈α∂to␈α⊂cross␈α∂rivers␈α∂unless␈α∂there␈α⊂is␈α∂something␈α∂wrong␈α⊂with␈α∂it.␈α∂ In␈α⊂particular,␈α∂we
␈↓ α∧␈↓haven't␈α⊂introduced␈α⊂into␈α∂our␈α⊂␈↓↓ontology␈↓␈α⊂(the␈α∂things␈α⊂that␈α⊂exist)␈α∂a␈α⊂category␈α⊂that␈α⊂includes␈α∂␈↓↓something
␈↓ α∧␈↓↓wrong␈α∞with␈α∂a␈α∞boat␈↓␈α∂or␈α∞a␈α∞category␈α∂that␈α∞includes␈α∂␈↓↓something␈α∞that␈α∞may␈α∂prevent␈α∞its␈α∂use␈↓.␈α∞ Incidentally,
␈↓ α∧␈↓once␈αwe␈αhave␈αdecided␈αto␈αadmit␈α␈↓↓something␈αwrong␈αwith␈αthe␈αboat␈↓,␈αwe␈αare␈αinclined␈αto␈αadmit␈αa␈α␈↓↓lack␈αof
␈↓ α∧␈↓↓oars␈↓␈α
as␈α
such␈α
a␈α
something␈α
and␈α
to␈α
ask␈α
questions␈α∞like,␈α
␈↓↓"Is␈α
a␈α
lack␈α
of␈α
oars␈α
all␈α
that␈α
is␈α
wrong␈α∞with␈α
the
␈↓ α∧␈↓↓boat?␈↓".
␈↓ α∧␈↓␈↓ u7


␈↓ α∧␈↓␈↓ αTI␈α∩imagine␈α∩that␈α∪many␈α∩philosophers␈α∩and␈α∩scientists␈α∪would␈α∩be␈α∩reluctant␈α∩to␈α∪introduce␈α∩such
␈↓ α∧␈↓␈↓↓things,␈↓␈α
but␈α
the␈αfact␈α
that␈α
ordinary␈α
language␈αallows␈α
␈↓↓"something␈α
wrong␈αwith␈α
the␈α
boat"␈↓␈α
suggests␈αthat
␈↓ α∧␈↓we␈α
shouldn't␈α
be␈α
hasty␈α
in␈α
excluding␈α
it.␈α
 Making␈α
a␈α
suitable␈α
formalism␈α
may␈α
be␈α
technically␈αdifficult
␈↓ α∧␈↓and philosophically problematical, but we must try.

␈↓ α∧␈↓␈↓ αTIn␈α
compensation,␈αwe␈α
may␈α
get␈αan␈α
increased␈αability␈α
to␈α
understand␈αnatural␈α
language,␈αbecause␈α
if
␈↓ α∧␈↓natural␈αlanguage␈αadmits␈αsomething␈αlike␈αminimal␈αreasoning,␈αit␈αis␈αunderstandable␈αthat␈αwe␈αwill␈αhave
␈↓ α∧␈↓difficulty in translating it into logical formalisms that don't.

␈↓ α∧␈↓␈↓ αTThe␈α⊗possibility␈α⊗of␈α⊗forming␈α⊗minimal␈α⊗completions␈α⊗of␈α⊗various␈α⊗parts␈α⊗of␈α⊗our␈α∃knowledge
␈↓ α∧␈↓introduces␈α∂a␈α∂kind␈α∂of␈α∂fuzziness␈α∂that␈α∂I␈α∂believe␈α∂may␈α∂prove␈α∂more␈α∂fruitful␈α∂than␈α∂that␈α∂explicated␈α∂by
␈↓ α∧␈↓fuzzy set theory.

␈↓ α∧␈↓␈↓ αTWhen␈αhumans␈α
and␈αmany␈α
recent␈αcomputer␈α
programs␈αreason␈α
from␈αa␈α
collection␈αof␈α
facts,␈αthey
␈↓ α∧␈↓often␈α
reach␈α
conclusions␈α
that␈α
depend␈α
on␈α
the␈αabsence␈α
of␈α
certain␈α
information.␈α
 For␈α
example,␈α
in␈αthe
␈↓ α∧␈↓absence␈α
of␈αinformation␈α
to␈α
the␈αcontrary,␈α
they␈αmay␈α
make␈α
default␈αassumptions.␈α
 Thus␈αif␈α
it␈α
is␈αstated
␈↓ α∧␈↓that␈α
a␈α
boat␈αis␈α
available␈α
at␈α
one␈αbank␈α
of␈α
a␈α
river,␈αit␈α
is␈α
often␈α
concluded␈αat␈α
least␈α
tentatively␈α
that␈αthe
␈↓ α∧␈↓boat␈αcan␈αbe␈αused␈αto␈αcross␈αthe␈αriver.␈α For␈αa␈αreason␈αshortly␈αto␈αbe␈αexplained,␈αwe␈αcall␈αsuch␈αreasoning
␈↓ α∧␈↓␈↓↓non-monotonic␈↓.


␈↓ α∧␈↓α␈↓ αTCo-ordinate systems and propositional calculus circumscription.

␈↓ α∧␈↓␈↓ αTSuppose␈α⊃we␈α⊃want␈α⊃to␈α⊂establish␈α⊃a␈α⊃language␈α⊃in␈α⊃which␈α⊂to␈α⊃express␈α⊃some␈α⊃class␈α⊃of␈α⊂assertions.
␈↓ α∧␈↓Deciding␈α∪on␈α∀predicate␈α∪and␈α∪function␈α∀symbols␈α∪and␈α∀their␈α∪meanings␈α∪in␈α∀order␈α∪to␈α∀express␈α∪these
␈↓ α∧␈↓assertions␈α
is␈α
like␈αchoosing␈α
a␈α
co-ordinate␈αsystem␈α
for␈α
a␈αphysical␈α
space.␈α
 For␈αexample,␈α
in␈α
the␈αblocks
␈↓ α∧␈↓world␈α
one␈αmay␈α
express␈α
everything␈αin␈α
terms␈α
of␈αthe␈α
relation␈α␈↓↓on(x,y,s)␈↓␈α
meaning␈α
that␈αblock␈α
␈↓↓x␈↓␈α
is␈αon
␈↓ α∧␈↓block␈α␈↓↓y␈↓␈αin␈αsituation␈α␈↓↓s,␈↓␈αbut␈αone␈αmight␈αalso␈αuse␈αthe␈αrelation␈α␈↓↓above(x,y,s)␈↓␈αthat␈αwould␈αbe␈αsatisfied␈αif
␈↓ α∧␈↓there␈αwere␈αintervening␈αblocks␈αin␈αbetween␈α␈↓↓x␈↓␈αand␈α␈↓↓y.␈↓␈αThe␈αsame␈αassertions␈αabout␈αblocks␈αcan␈αbe␈α
made
␈↓ α∧␈↓in␈α
in␈α
either␈α
language.␈α
 In␈α
particular,␈α
each␈α
can␈αbe␈α
defined␈α
in␈α
terms␈α
of␈α
the␈α
other,␈α
and␈αequivalent␈α
sets
␈↓ α∧␈↓of␈αaxioms␈αcan␈αbe␈αwritten.␈α (I␈αdon't␈αknow␈αof␈αany␈αgeneral␈αstudy␈αof␈α"logical␈αco-ordinate␈αsystems"␈αand
␈↓ α∧␈↓their␈α
relations␈α∞and␈α
transformations.␈α∞ It␈α
will␈α∞certainly␈α
be␈α
more␈α∞complex␈α
than␈α∞the␈α
theory␈α∞of␈α
linear
␈↓ α∧␈↓transformations of vector spaces).

␈↓ α∧␈↓␈↓ αTLogical␈αco-ordinate␈α
systems␈αthat␈α
are␈αequivalent␈α
in␈αterms␈αof␈α
what␈αcan␈α
be␈αexpressed␈α
may␈αbe
␈↓ α∧␈↓inequivalent␈α⊃heuristically.␈α⊂ Conjectures␈α⊃that␈α⊂are␈α⊃natural␈α⊂in␈α⊃one␈α⊂system␈α⊃may␈α⊂seem␈α⊃contrived␈α⊂in
␈↓ α∧␈↓others.␈α In␈αparticular,␈αcircumscription␈αyields␈αdifferent␈αconjectures␈αin␈αdifferent␈αco-ordinate␈αsystems.
␈↓ α∧␈↓A propositional calculus version of circumscription illustrates some of the issues.

␈↓ α∧␈↓␈↓ αTSuppose␈α⊗we␈α⊗want␈α⊗a␈α⊗propositional␈α⊗language␈α⊗for␈α⊗expressing␈α⊗a␈α⊗class␈α⊗of␈α⊗assertions.␈α⊗ A
␈↓ α∧␈↓propositional␈α∞language␈α∞is␈α∞established␈α∞by␈α∞choosing␈α∞propositional␈α∞letters␈α∞␈↓↓p␈↓β1␈↓↓,...,p␈↓βn␈↓␈α∂and␈α∞regarding
␈↓ α∧␈↓each␈αof␈αthem␈αas␈αexpressing␈αsome␈αelementary␈αfact.␈α We␈αmay␈αthen␈αexpress␈αthe␈αset␈α␈↓↓A␈↓␈αof␈αknown␈αfacts
␈↓ α∧␈↓as␈α
a␈α
sentence␈α
␈↓↓AX␈↓␈α
in␈α
terms␈α
of␈α
the␈α
␈↓↓p␈↓'s.␈α
 A␈α
model␈α
of␈α
the␈α
facts␈α
is␈α
any␈α
assignment␈α
of␈α
truth␈α
values␈αto␈α
the
␈↓ α∧␈↓␈↓↓p␈↓βi␈↓'s that makes ␈↓↓AX␈↓ true.

␈↓ α∧␈↓␈↓ αTAs␈α
a␈αsimple␈α
example,␈αwe␈α
may␈αbe␈α
thinking␈αof␈α
assertions␈α␈↓↓p,␈↓␈α
␈↓↓q,␈↓␈αand␈α
␈↓↓r␈↓␈αrelated␈α
by␈α␈↓↓p ≡ (q ≡ r)␈↓.
␈↓ α∧␈↓and␈α
satisfying␈α␈↓↓p ∨ r␈↓.␈α
 One␈α
co-ordinate␈αsystem␈α
would␈αtake␈α
␈↓↓p␈↓β1␈↓↓ = p␈↓␈α
and␈α␈↓↓p␈↓β2␈↓↓ = q␈↓,␈α
and␈α
another␈αwould
␈↓ α∧␈↓take ␈↓↓p␈↓β1␈↓↓' = q␈↓ and ␈↓↓p␈↓β2␈↓↓' = ¬(p ≡ r)␈↓.  In one system we would have the axiom ␈↓↓p␈↓β1␈↓↓

␈↓ α∧␈↓␈↓ αTLet ␈↓↓M1␈↓ and ␈↓↓M2␈↓ be models of ␈↓↓AX.␈↓ We define
␈↓ α∧␈↓␈↓ u8


␈↓ α∧␈↓␈↓ αT␈↓↓M1 ≤ M2 ≡ ∀i.(true(p␈↓βi␈↓↓,M2) ⊃ true(p␈↓βi␈↓↓,M1))␈↓.

␈↓ α∧␈↓␈↓ αTA␈α⊂minimal␈α∂model␈α⊂is␈α⊂one␈α∂that␈α⊂is␈α⊂not␈α∂a␈α⊂proper␈α∂extension,␈α⊂i.e.␈α⊂a␈α∂model␈α⊂in␈α⊂which␈α∂(roughly
␈↓ α∧␈↓speaking)␈α
as␈α∞many␈α
of␈α
the␈α∞␈↓↓p␈↓βi␈↓s␈α
as␈α∞possible␈α
are␈α
false␈α∞-␈α
consistent␈α∞with␈α
the␈α
truth␈α∞of␈α
␈↓↓AX␈↓.␈α∞ ␈↓↓Note␈α
that
␈↓ α∧␈↓↓while␈α
the␈α
models␈α∞of␈α
a␈α
set␈α∞of␈α
facts␈α
are␈α∞independent␈α
of␈α
the␈α∞co-ordinate␈α
system,␈α
the␈α∞minimal␈α
models
␈↓ α∧␈↓↓depend␈α∂on␈α∞the␈α∂co-ordinate␈α∞system␈↓.␈α∂ Here␈α∞is␈α∂the␈α∂most␈α∞trivial␈α∂example.␈α∞ Let␈α∂there␈α∞be␈α∂one␈α∂letter␈α∞␈↓↓p␈↓
␈↓ α∧␈↓representing␈αthe␈αone␈αfact␈αin␈αa␈αco-ordinate␈αsystem␈α␈↓↓C,␈↓␈αand␈αlet␈α␈↓↓A␈↓␈αbe␈αthe␈αnull␈αset␈αof␈αfacts␈αso␈αthat␈α␈↓↓AX␈↓
␈↓ α∧␈↓is␈α⊂the␈α⊂sentence␈α∂␈↓↓T␈↓␈α⊂(identically␈α⊂true).␈α⊂ The␈α∂one␈α⊂other␈α⊂co-ordinate␈α∂system␈α⊂␈↓↓C'␈↓␈α⊂uses␈α⊂the␈α∂elementary
␈↓ α∧␈↓sentence␈α␈↓↓p'␈↓␈αtaken␈αequivalent␈αto␈α␈↓↓¬p␈↓.␈α The␈αminimal␈αmodel␈αof␈α␈↓↓C␈↓␈αis␈α{¬p},␈αand␈αthe␈αminimal␈αmodel␈αof
␈↓ α∧␈↓␈↓↓C'␈↓␈α
is␈α
{p}.␈α Since␈α
minimal␈α
reasoning␈αdepends␈α
on␈α
the␈αco-ordinate␈α
system␈α
and␈αnot␈α
merely␈α
on␈αthe␈α
facts
␈↓ α∧␈↓expressed␈α⊂in␈α⊃the␈α⊂axioms,␈α⊃the␈α⊂utility␈α⊃of␈α⊂an␈α⊃axiom␈α⊂system␈α⊃will␈α⊂depend␈α⊃on␈α⊂whether␈α⊃its␈α⊂minimal
␈↓ α∧␈↓models express the uses we wish to make of Occam's razor.

␈↓ α∧␈↓␈↓ αTA␈α∪less␈α∩trivial␈α∪example␈α∩of␈α∪minimal␈α∩entailment␈α∪is␈α∩the␈α∪following.␈α∩ The␈α∪propositional␈α∩co-
␈↓ α∧␈↓ordinate␈α
system␈α∞has␈α
basic␈α
sentences␈α∞␈↓↓p␈↓β1␈↓,␈α
␈↓↓p␈↓β2␈↓␈α
and␈α∞␈↓↓p␈↓β3␈↓,␈α
and␈α
␈↓↓AX␈α∞=␈α
p␈↓β1␈↓↓␈α
∨␈α∞p␈↓β2␈↓.␈α
 There␈α
are␈α∞two␈α
minimal
␈↓ α∧␈↓models.␈α
 ␈↓↓p␈↓β3␈↓␈α
is␈α
false␈αin␈α
both,␈α
and␈α
␈↓↓p␈↓β1␈↓␈αis␈α
false␈α
in␈α
one,␈αand␈α
␈↓↓p␈↓β2␈↓␈α
is␈α
false␈αin␈α
the␈α
other.␈α
 Thus␈α
we␈αhave
␈↓ α∧␈↓␈↓↓AX ␈↓πq␈↓βm␈↓↓ (¬(p␈↓β1␈↓↓ ∧ p␈↓β2␈↓↓) ∧ ¬p␈↓β3␈↓).

␈↓ α∧␈↓␈↓ αTNote␈α
that␈αif␈α
␈↓↓AX␈↓␈αis␈α
a␈α
conjunction␈αof␈α
certain␈αelementary␈α
sentences␈α
(some␈αof␈α
them␈αnegated),␈α
e.g.
␈↓ α∧␈↓␈↓↓AX = p␈↓β2␈↓↓ ∧ ¬p␈↓β4␈↓,␈α∂then␈α⊂there␈α∂is␈α⊂a␈α∂unique␈α⊂minimal␈α∂model,␈α⊂but␈α∂if,␈α⊂as␈α∂above,␈α⊂␈↓↓AX = p␈↓β2␈↓↓ ∨ ¬p␈↓β4␈↓,␈α∂then
␈↓ α∧␈↓there is more than one minimal model.

␈↓ α∧␈↓␈↓ αTOne may also consider extensions ␈↓↓relative␈↓ to a set ␈↓↓B␈↓ of elementary sentences.  We have

␈↓ α∧␈↓␈↓ αT␈↓↓M1 ≤ M2 (mod B) ≡ ∀p.(p ε B ∧ true(p,M1) ⊃ true(p,M2)␈↓.

␈↓ α∧␈↓␈↓ αTWe␈α∪can␈α∀then␈α∪introduce␈α∀minimal␈α∪models␈α∪relative␈α∀to␈α∪␈↓↓B␈↓␈α∀and␈α∪the␈α∀corresponding␈α∪relative
␈↓ α∧␈↓minimal␈αentailment.␈α Thus␈αwe␈αmay␈αcare␈α
about␈αminimality␈αand␈αOccam's␈αrazor␈αonly␈αover␈α
a␈αcertain
␈↓ α∧␈↓part of our knowledge.

␈↓ α∧␈↓␈↓ αTNote␈α⊂that␈α⊂we␈α⊂may␈α⊂discover␈α⊂a␈α⊂set␈α⊂of␈α⊂facts␈α⊂one␈α⊂at␈α⊂a␈α⊂time␈α⊂so␈α⊂that␈α⊂we␈α⊂have␈α⊂an␈α⊂increasing
␈↓ α∧␈↓sequence␈α⊂␈↓↓A␈↓β1␈↓↓␈α⊂⊂␈α⊂A␈↓β2␈↓␈α⊂⊂␈α⊂...␈α⊂of␈α⊂sets␈α⊂of␈α⊂sentences.␈α⊂ A␈α⊂given␈α⊂sentence␈α⊂␈↓↓p␈↓␈α⊂may␈α⊂oscillate␈α⊂in␈α⊃its␈α⊂minimal
␈↓ α∧␈↓entailment␈α∂by␈α∞the␈α∂␈↓↓A␈↓βi␈↓,␈α∞e.g.␈α∂we␈α∞may␈α∂have␈α∂␈↓↓A␈↓β1␈↓π q␈↓βm␈↓↓ p␈↓,␈α∞␈↓↓A␈↓β2␈↓π q␈↓βm␈↓↓ ¬p␈↓,␈α∂neither␈α∞may␈α∂be␈α∞entailed␈α∂by␈α∂␈↓↓A␈↓β3␈↓,␈α∞etc.
␈↓ α∧␈↓The␈α
common␈α∞sense␈α
Occam's␈α∞razor␈α
conclusion␈α
about␈α∞a␈α
sentence␈α∞␈↓↓p␈↓␈α
often␈α
behaves␈α∞this␈α
way␈α∞as␈α
our
␈↓ α∧␈↓knowledge increases.

␈↓ α∧␈↓␈↓ αTReasons␈α
can␈α
be␈α
used␈α
to␈αreduce␈α
propositional␈α
circumscription␈α
to␈α
domain␈αcircumscription.␈α
 We
␈↓ α∧␈↓introduce␈αfor␈αeach␈α
propositional␈αletter␈α␈↓↓p␈↓βi␈↓␈αto␈α
be␈αminimized␈αa␈α
corresponding␈αpredicate␈α␈↓↓pr␈↓βi␈↓↓(r)␈↓␈αand␈α
the
␈↓ α∧␈↓axiom

␈↓ α∧␈↓␈↓ αT1)␈↓ αt ␈↓↓p␈↓βi␈↓↓ ≡ ∃r.pr␈↓βi␈↓↓(r)␈↓,

␈↓ α∧␈↓␈↓ αTwhich asserts that ␈↓↓p␈↓βi␈↓ is true only if there is a reason why.  We also need axioms

␈↓ α∧␈↓␈↓ αT2)␈↓ αt ␈↓↓∀r.¬(pr␈↓βi␈↓↓(r) ∧ pr␈↓βj␈↓↓(r))␈↓

␈↓ α∧␈↓␈↓ αTfor␈αeach␈α
␈↓↓i␈↓␈αand␈α
␈↓↓j␈↓␈αand␈α
axioms␈αasserting␈αthat␈α
reasons␈α␈↓↓r␈↓␈α
are␈αdistinct␈α
from␈αany␈αother␈α
individuals.
␈↓ α∧␈↓A␈α∞minimal␈α
model␈α∞will␈α
then␈α∞have␈α
as␈α∞few␈α
reasons␈α∞as␈α
possible␈α∞and␈α
hence␈α∞will␈α
minimize␈α∞the␈α∞set␈α
of
␈↓ α∧␈↓true ␈↓↓p␈↓βi␈↓s.
␈↓ α∧␈↓␈↓ u9


␈↓ α∧␈↓α␈↓ αTCircumscription in the Blocks World

␈↓ α∧␈↓␈↓ αTHere␈α
is␈αa␈α
formalization␈αof␈α
the␈αblocks␈α
world␈αin␈α
which␈αcircumscription␈α
is␈αused␈α
to␈α
keep␈αopen
␈↓ α∧␈↓the␈α
set␈α
of␈α
possible␈α
circumstances␈α
that␈α
may␈α
prevent␈α
a␈α
block␈α
␈↓↓x␈↓␈α
from␈α
being␈α
moved␈α
onto␈α
a␈α∞block␈α
␈↓↓y.␈↓
␈↓ α∧␈↓We use the situation calculus of (McCarthy and Hayes 1969).

␈↓ α∧␈↓␈↓ αTA␈α
situation␈α
␈↓↓s␈↓␈α
is␈α
a␈α
snapshot␈α
of␈α
the␈α
world␈α
at␈α
an␈α
instant␈α
of␈α
time.␈α
 We␈α
write␈α
␈↓↓on(x,y,s)␈↓␈α
to␈αsay
␈↓ α∧␈↓that␈αblock␈α␈↓↓x␈↓␈αis␈αon␈αblock␈α␈↓↓y␈↓␈αin␈αsituation␈α␈↓↓s.␈↓␈α␈↓↓s' = result(a,s)␈↓␈αis␈αthe␈αnew␈αsituation␈α␈↓↓s'␈↓␈αthat␈αresults␈αwhen
␈↓ α∧␈↓action␈α
␈↓↓a␈↓␈α
is␈α
performed␈αin␈α
situation␈α
␈↓↓s.␈↓␈α
One␈αsuch␈α
action␈α
is␈α
␈↓↓move(x,y),␈↓␈αan␈α
attempt␈α
to␈α
move␈α
block␈α␈↓↓x␈↓
␈↓ α∧␈↓onto block ␈↓↓y.␈↓ The effect of this action is given by

␈↓ α∧␈↓␈↓ αT3)␈↓ αt ␈↓↓∀x y s.(∀r.¬prevmove(r,x,y,s) ⊃ on(x,y,result(move(x,y),s)))␈↓

␈↓ α∧␈↓␈↓ αTwhich asserts that ␈↓↓x␈↓ is on ␈↓↓y␈↓ after the move if there is no reason ␈↓↓r␈↓ that prevents the move.

␈↓ α∧␈↓␈↓ αTSuppose␈αthat␈αone␈αreason␈αwhy␈αa␈αblock␈α␈↓↓x␈↓␈αmight␈αnot␈αbe␈αmovable␈αis␈αif␈αit␈αwere␈αtoo␈αheavy.␈α We
␈↓ α∧␈↓express this by

␈↓ α∧␈↓␈↓ αT4)␈↓ αt ␈↓↓∀x y r s.(tooheavy x ⊃ prevmove(heaviness x,x,y,s))␈↓,

␈↓ α∧␈↓␈↓ αTusing␈αboth␈αthe␈αpredicate␈α
␈↓↓tooheavy␈↓␈αand␈αthe␈αabstract␈αentity␈α
␈↓↓heaviness x␈↓␈αwhich␈αcan␈αbe␈αa␈α
reason.
␈↓ α∧␈↓Here are some axioms about reasons:

␈↓ α∧␈↓␈↓ αT5)␈↓ αt ␈↓↓∀x.(¬tooheavy x ⊃ heaviness x = JUNK)␈↓,

␈↓ α∧␈↓␈↓ αT6)␈↓ αt ␈↓↓¬isreason JUNK␈↓,

␈↓ α∧␈↓␈↓ αTand

␈↓ α∧␈↓␈↓ αT7)␈↓ αt ␈↓↓∀r x y s.(prevmove(r,x,y,s) ⊃ isreason r)␈↓.

␈↓ α∧␈↓␈↓ αTWe␈α⊃must␈α⊃also␈α⊃be␈α⊃able␈α⊃to␈α⊃ensure␈α⊃that␈α⊃blocks,␈α⊃situations,␈α⊃actions,␈α⊃the␈α⊃object␈α⊃␈↓↓JUNK␈↓␈α⊃and
␈↓ α∧␈↓reasons␈αare␈α
mutually␈αdisjoint.␈α This␈α
can␈αeither␈αbe␈α
done␈αby␈αappropriate␈α
axioms␈αor␈α
more␈αelegantly
␈↓ α∧␈↓by␈αusing␈αa␈α
many␈αsorted␈αlogic␈α
in␈αwhich␈αvariables␈αranging␈α
over␈αthese␈αclasses␈α
are␈αdeclared␈αto␈α
be␈αof
␈↓ α∧␈↓appropriate distinct sorts.

␈↓ α∧␈↓␈↓ αTNow␈α
suppose␈α
that␈α
we␈α∞have␈α
blocks␈α
␈↓↓A␈↓␈α
and␈α
␈↓↓B,␈↓␈α∞and␈α
we␈α
apply␈α
the␈α
circumscription␈α∞schema␈α
to
␈↓ α∧␈↓the␈αabove␈αaxioms␈αand␈αthe␈αconstants␈α␈↓↓A,␈↓␈α␈↓↓B,␈↓␈α␈↓↓JUNK␈↓␈αand␈αan␈αinitial␈αsituation␈α␈↓↓S0.␈↓␈αThe␈αschema␈αwill
␈↓ α∧␈↓allow␈α∞us␈α∞to␈α∞prove␈α∞␈↓↓on(x,y,result(move(x,y,S0))␈↓,␈α∂because␈α∞the␈α∞minimal␈α∞model␈α∞will␈α∞not␈α∂contain␈α∞any
␈↓ α∧␈↓reason␈α
why␈α
␈↓↓x␈↓␈α
cannot␈α
be␈α
moved␈α
onto␈α
␈↓↓y.␈↓␈α
In␈α
this␈α
minimal␈α
model,␈α
␈↓↓heaviness x ␈↓␈α
will␈α
have␈α∞the␈α
value
␈↓ α∧␈↓␈↓↓JUNK.␈↓

␈↓ α∧␈↓␈↓ αTNEW START

␈↓ α∧␈↓␈↓ αTLet's␈α∞begin␈α∞with␈α∞a␈α∞static␈α∞world,␈α∞in␈α∞which␈α∞we␈α∞want␈α∞to␈α∞use␈α∞circumscription␈α∞to␈α∞avoid␈α∞stating
␈↓ α∧␈↓more on-ness relations than necessary.  Specifically, we would like circumscription to give us

␈↓ α∧␈↓␈↓ αT1. A block is clear ucee (unless contrary evidence exists).

␈↓ α∧␈↓␈↓ αT2. A block is on the table ucee.
␈↓ α∧␈↓␈↓ f10


␈↓ α∧␈↓␈↓ αT3. Only those blocks exist for which there is evidence.


␈↓ α∧␈↓α␈↓ αTComparison with other formalisms

␈↓ α∧␈↓␈↓ αT1. Default cases.  Many programs provide default cases.

␈↓ α∧␈↓␈↓ αT1.␈α∩Maybe␈α∩we␈α∩can␈α∩consider␈α∩propositional␈α⊃and␈α∩domain␈α∩circumscription␈α∩as␈α∩instances␈α∩of␈α⊃a
␈↓ α∧␈↓common␈αconcept␈αif␈αwe␈αallow␈αourselves␈αto␈αintroduce␈αan␈αarbitrary␈αpartial␈αordering␈αof␈αmodels␈αof␈αsets
␈↓ α∧␈↓of␈α∂sentences␈α∞and␈α∂consider␈α∞minimal␈α∂models␈α∞with␈α∂respect␈α∞to␈α∂this␈α∞ordering.␈α∂ We␈α∞probably␈α∂want␈α∞to
␈↓ α∧␈↓restrict␈α∪the␈α∪ordering␈α∀so␈α∪that␈α∪there␈α∀will␈α∪be␈α∪some␈α∀syntactic␈α∪counterpart␈α∪of␈α∀minimal␈α∪inference.
␈↓ α∧␈↓Actually␈α⊂propositional␈α⊃circumscription␈α⊂doesn't␈α⊃meet␈α⊂this␈α⊃requirement␈α⊂without␈α⊃modification,␈α⊂but
␈↓ α∧␈↓anyway it's desirable.

␈↓ α∧␈↓␈↓ αT2.␈αPerhaps␈αthe␈αright␈αway␈αto␈αreduce␈αpropositional␈αcircumscription␈αto␈αdomain␈αcircumscription
␈↓ α∧␈↓is␈α
to␈αreplace␈α
each␈αpropositional␈α
variable␈α
␈↓↓p␈↓βi␈↓␈αby␈α
the␈αwff␈α
␈↓↓∃x.(index␈α
x␈α=␈α
i)␈↓.␈α In␈α
that␈α
way␈αminimizing
␈↓ α∧␈↓the␈αtruth␈αof␈αthe␈αproposition␈αis␈αaccomplished␈αby␈αminimizing␈αthe␈αexistence␈αof␈αthe␈α␈↓↓x␈↓'s.␈α The␈αpurpose
␈↓ α∧␈↓of␈α␈↓↓index␈αx␈α=␈αi␈↓␈αis␈αto␈αmake␈αsure␈αthat␈αthe␈αexistence␈αof␈αthe␈α␈↓↓x␈↓'s␈αcan␈αbe␈αminimized␈αseparately.␈α We␈αneed
␈↓ α∧␈↓to␈α
be␈α
sure␈α∞that␈α
no␈α
other␈α∞object␈α
has␈α
an␈α
integer␈α∞index,␈α
but␈α
we␈α∞can␈α
introduce␈α
axioms␈α∞that␈α
require
␈↓ α∧␈↓them all to have the non-integer JUNK as index.

␈↓ α∧␈↓␈↓ αTThis␈αraises␈αthe␈αproblem␈αof␈αwhether␈αthere␈αis␈αan␈αanalogous␈αway␈αof␈αtreating␈αpredicates␈α␈↓↓p(u,v)␈↓.
␈↓ α∧␈↓Maybe␈αwe␈αwant␈αto␈αreplace␈αit␈αby␈α␈↓↓∃x.(p'(u,v,x) ∧ index x = i)␈↓␈αor␈αperhaps␈αistead␈αof␈α␈↓↓ = i␈↓,␈αwe␈αshould
␈↓ α∧␈↓have ␈↓↓ = <u,v,i>␈↓.

␈↓ α∧␈↓␈↓ αT3. CIRCUM[1,CLT] is the following example:

␈↓ α∧␈↓␈↓ αTConsider the following problem (told to CLT by DrewMcD, ascribed to Bmoore):

␈↓ α∧␈↓␈↓ αTYou␈α∞are␈α∞told␈α∞that␈α∞the␈α∞only␈α∞things␈α∞on␈α∞the␈α∞table␈α∞are␈α∞things␈α∞that␈α∞you␈α∞can␈α∞prove␈α∞are␈α∂on␈α∞the
␈↓ α∧␈↓table.␈α⊂ Further␈α⊃you␈α⊂are␈α⊃told␈α⊂that␈α⊃A␈α⊂is␈α⊃on␈α⊂the␈α⊂table␈α⊃and␈α⊂B␈α⊃is␈α⊂on␈α⊃the␈α⊂table␈α⊃and␈α⊂that␈α⊃there␈α⊂is
␈↓ α∧␈↓something␈α
red␈α
on␈α
the␈α
table.␈α
 You␈αwould␈α
like␈α
to␈α
be␈α
able␈α
to␈α
conclude␈αthat␈α
either␈α
A␈α
is␈α
red␈α
or␈α
B␈αis
␈↓ α∧␈↓red.

␈↓ α∧␈↓␈↓ αTCircumscription␈α⊃can␈α⊂be␈α⊃applied␈α⊂to␈α⊃solve␈α⊂this␈α⊃problem.␈α⊂ We␈α⊃formalize␈α⊂the␈α⊃problem␈α⊃in␈α⊂a
␈↓ α∧␈↓language L=<<Ontable,Red>,<>,<A,B>> where Ontable and Red are unary.  The theory is:

␈↓ α∧␈↓␈↓ αT(1) Ontable(A)

␈↓ α∧␈↓␈↓ αT(2) Ontable(B)

␈↓ α∧␈↓␈↓ αT(3) ∃x.(Ontable(x)∧Red(x))

␈↓ α∧␈↓␈↓ αTCircumscribing with respect to (1) and (2) we obtain the schema:

␈↓ α∧␈↓␈↓ αT(4) PHI(A)∧PHI(B) ⊃ ∀x.PHI(x)

␈↓ α∧␈↓␈↓ αTand it is easy to jump to the conclusion that

␈↓ α∧␈↓␈↓ αT(5) ∀x.(x=A∨x=B)
␈↓ α∧␈↓␈↓ f11


␈↓ α∧␈↓␈↓ αTand thus to conclude that Red(A)∨Red(B).

␈↓ α∧␈↓␈↓ αTNotice␈α⊃that␈α∩if␈α⊃the␈α∩circumscription␈α⊃is␈α∩done␈α⊃with␈α∩respect␈α⊃to␈α∩all␈α⊃three␈α∩facts␈α⊃then␈α∩we␈α⊃lose.
␈↓ α∧␈↓Namely we get the schema

␈↓ α∧␈↓␈↓ αT(6) PHI(A)∧PHI(B)∧∃x.(PHI(x)∧Ontable(x)∧Red(x)) ⊃ ∀x.PHI(x)

␈↓ α∧␈↓␈↓ αTthen we only conclude

␈↓ α∧␈↓␈↓ αT(7) ∀x.(x=A∨x=B∨Red(x))

␈↓ α∧␈↓␈↓ αTwhich does not allow us to show that either A or B is red.

␈↓ α∧␈↓␈↓ αT4.␈α⊃The␈α∩essence␈α⊃of␈α∩the␈α⊃Moore-McDermott␈α⊃example␈α∩is␈α⊃included␈α∩in␈α⊃the␈α∩following␈α⊃simpler
␈↓ α∧␈↓example.

␈↓ α∧␈↓␈↓ αTThere␈αis␈αone␈αconstant␈αA␈αand␈αone␈αsentence␈α∃x.Red(x).␈α Circumscribing␈αon␈αthe␈α
constant␈αonly
␈↓ α∧␈↓gives␈α∞PHI(A)␈α
⊃␈α∞∀x.PHI(x)␈α∞and␈α
specializing␈α∞PHI␈α∞by␈α
∀x.(PHI(x)␈α∞≡␈α
x␈α∞=␈α∞A)␈α
establishes␈α∞∀x.(x␈α∞=␈α
A)
␈↓ α∧␈↓from which Red(A) follows.  Circumscribing on both A and ∃x.Red(x) gives

␈↓ α∧␈↓␈↓ αTPHI(A) ∧ ∃x.(PHI(x) ∧ Red(x)) ⊃ ∀x.PHI(x)

␈↓ α∧␈↓␈↓ αTfrom which it doesn't look like we can infer Red(A).

␈↓ α∧␈↓␈↓ αTIt␈α∂looks␈α∂like␈α∞circumscription␈α∂doesn't␈α∂give␈α∞us␈α∂what␈α∂is␈α∞true␈α∂in␈α∂all␈α∞minimal␈α∂models␈α∂but␈α∞only
␈↓ α∧␈↓what␈αis␈αtrue␈αin␈αall␈αminimal␈αmodels␈αcontained␈αin␈αarbitrary␈αmodels,␈αi.e.␈αa␈αsentence␈αp␈αis␈αprovable␈αby
␈↓ α∧␈↓circumscribing␈αa␈αset␈αof␈αsentences␈αA␈αiff␈αevery␈αmodel␈αM␈αof␈αA␈αis␈αsuch␈αthat␈αevery␈αminimal␈αmodel␈αM'
␈↓ α∧␈↓of␈αA␈αcontained␈αin␈αM␈αsatisfies␈αp.␈α THE␈αABOVE␈αWAS␈αA␈αMISTAKE.␈α At␈αleast␈αin␈αthe␈αabove␈αcase
␈↓ α∧␈↓the model with two objects - A and a red one - is indeed minimal w/r {A , ∃x.Red(x)}.

␈↓ α∧␈↓␈↓ αT5.␈αImitation␈αsemantics.␈α Suppose␈αwe␈αreplace␈αsome␈αof␈αthe␈αpredicate␈αsymbols␈αof␈αa␈αtheory␈αby␈αa
␈↓ α∧␈↓new␈αsymbols␈αwith␈αone␈αmore␈αargument␈α-␈αa␈αworld.␈α Thus␈αRed(x)␈αis␈αreplaced␈αby␈αRed(x,w).␈α Some␈αof
␈↓ α∧␈↓the␈α∞properties␈α∞of␈α
model␈α∞theory␈α∞can␈α∞now␈α
be␈α∞axiomatized␈α∞within␈α∞the␈α
theory.␈α∞ The␈α∞process␈α∞can␈α
be
␈↓ α∧␈↓repeated␈α⊂by␈α⊃adding␈α⊂another␈α⊂"outer"␈α⊃world␈α⊂parameter,␈α⊂but␈α⊃we␈α⊂shall␈α⊂discuss␈α⊃only␈α⊂a␈α⊃single␈α⊂such
␈↓ α∧␈↓"semanticization" to begin with.

␈↓ α∧␈↓␈↓ αTEvery␈αterm␈αand␈α
wff␈αnow␈αdepends␈αon␈α
w␈α-␈αassuming,␈α
as␈αwe␈αshall␈αfor␈α
now,␈αthat␈αwe␈αapply␈α
each
␈↓ α∧␈↓predicate␈α⊂to␈α∂the␈α⊂same␈α∂variable␈α⊂w␈α∂as␈α⊂we␈α∂build␈α⊂up␈α∂the␈α⊂wffs.␈α∂ We␈α⊂can␈α∂quantify␈α⊂over␈α∂w,␈α⊂so␈α∂that
␈↓ α∧␈↓∀w.<wff>␈α⊃will␈α∩enjoy␈α⊃some␈α⊃of␈α∩the␈α⊃properties␈α⊃of␈α∩validity␈α⊃and␈α⊃∃w.<wff>␈α∩will␈α⊃have␈α⊃some␈α∩of␈α⊃the
␈↓ α∧␈↓properties of satisfiability.

␈↓ α∧␈↓␈↓ αTHow␈α⊃to␈α∩axiomatize␈α⊃w␈α∩is␈α⊃not␈α∩immediately␈α⊃obvious.␈α⊃ One␈α∩idea␈α⊃is␈α∩to␈α⊃imagine␈α∩a␈α⊃common
␈↓ α∧␈↓domain␈α∞of␈α∞non-w␈α
s␈α∞and␈α∞introduce␈α∞a␈α
predicate␈α∞exists(x,w).␈α∞ (I␈α∞confess␈α
a␈α∞weakness␈α∞for␈α∞theories␈α
in
␈↓ α∧␈↓which something like existence is a predicate).  This allows a definition of ordering

␈↓ α∧␈↓␈↓ αT␈↓↓w1 < w2 ≡ ∀x.(exists(x,w1) ⊃ exists(x,w2))
␈↓ α∧␈↓␈↓ αT∧ ∀xy.(exists(x,w1) ∧ exists(y,w1) ⊃ (P(x,y,w1) ≡ P(x,y,w2))
␈↓ α∧␈↓␈↓ αT∧ ...
␈↓ α∧␈↓␈↓ f12


␈↓ α∧␈↓␈↓ αTwhere␈α...␈αindicates␈α
that␈αthere␈αis␈αa␈α
wff␈αsimilar␈αto␈α
that␈αon␈αthe␈αsecond␈α
line␈αfor␈αeach␈αpredicate␈α
in
␈↓ α∧␈↓the language.  This will permit us to define minimal worlds.

␈↓ α∧␈↓␈↓ αTOur␈αability␈αto␈αimitate␈αreal␈αmodel␈αtheory␈αwill␈αdepend␈αon␈αour␈αtools␈αfor␈αasserting␈αthe␈αexistence
␈↓ α∧␈↓of␈α∞enough␈α∞worlds.␈α∞ If␈α
the␈α∞domain␈α∞is␈α∞infinite␈α
and␈α∞there␈α∞is␈α∞even␈α
one␈α∞unary␈α∞predicate␈α∞symbol,␈α
the
␈↓ α∧␈↓number␈α∪of␈α∪interpretations␈α∩is␈α∪already␈α∪non-denumerable,␈α∩and␈α∪the␈α∪Lowenheim-Skolem␈α∩theorem
␈↓ α∧␈↓already tells us that no axiomatization can insure that.

␈↓ α∧␈↓␈↓ αTA␈α
certain␈α
amount␈α
can␈α
be␈α
done␈α
by␈α
postulating␈α
that␈α
for␈α
every␈α
world␈α
w␈α
there␈α
is␈α
a␈α
world␈α
w'␈α
that
␈↓ α∧␈↓gives␈α
the␈α
same␈α
value␈α
to␈α
all␈α
predicates␈α
except␈α
that␈α
a␈α
single␈α
predicate␈α
has␈α
a␈α
single␈α
value␈αchanged.
␈↓ α∧␈↓We␈α
can␈α
also␈α
imagine␈α
other␈α
changes␈α
whose␈α∞possibility␈α
can␈α
be␈α
stated.␈α
 The␈α
main␈α
purpose␈α∞of␈α
such
␈↓ α∧␈↓axiomatizations␈α↔will␈α⊗be␈α↔to␈α⊗insure␈α↔that␈α⊗certain␈α↔formulas␈α⊗or␈α↔at␈α⊗least␈α↔enough␈α↔formulas␈α⊗are
␈↓ α∧␈↓"satisfiable".

␈↓ α∧␈↓␈↓ αT"Completeness" can also be defined as asserting that all "valid" formulas are provable.

␈↓ α∧␈↓␈↓ αTI think all this is related to circumscription, but I can't now make the connection.

␈↓ α∧␈↓␈↓ αT6. Propositional circumscription can be done by introducing worlds as follows:

␈↓ α∧␈↓␈↓ αTEach propositional variable ␈↓↓p␈↓βi␈↓ is replaced by a function ␈↓↓p␈↓βi␈↓↓(w)␈↓.

␈↓ α∧␈↓␈↓ αTWe write

␈↓ α∧␈↓␈↓ αT␈↓↓w1 ≤ w2 ≡ ∀i.[p␈↓βi␈↓↓(w1) ⊃ p␈↓βi␈↓↓(w2)]␈↓

␈↓ α∧␈↓␈↓ αTwhere␈αwe␈αmay␈αsuppose␈αthat␈αthe␈αquantification␈αover␈α␈↓↓i␈↓␈αactually␈αdesignates␈αa␈αconjunction␈αover
␈↓ α∧␈↓the set of propositional variables to be circumscribed.

␈↓ α∧␈↓␈↓ αTMinimality is defined by

␈↓ α∧␈↓␈↓ αT␈↓↓minimal w ≡ ∀w1.(w1 ≤ w ⊃ w1 = w)␈↓.

␈↓ α∧␈↓␈↓ αTA wff in the original formulation becomes a ␈↓↓wff(w)␈↓ in the new.  We write ␈↓↓wff1 ␈↓πq␈↓↓ wff2␈↓ if

␈↓ α∧␈↓␈↓ αT␈↓↓∀w.(wff1(w) ∧ minimal w ⊃ wff2(w))␈↓.

␈↓ α∧␈↓␈↓ αTThis version of MINIMA.NEW[S79,JMC] PUBbed at 13:07 on June 18, 1979.